/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

#pragma once

#ifdef HAVE_AUTOCONF
#include <autoconf.h>
#endif /* HAVE_AUTOCONF */
/*Z 架构相关的seL4内核对象类型 */
typedef enum _mode_object {
    seL4_X86_PDPTObject = seL4_NonArchObjectTypeCount,/*Z 二级页表 */
    seL4_X64_PML4Object,        /*Z 一级页表 */
#ifdef CONFIG_HUGE_PAGE
    seL4_X64_HugePageObject,    /*Z 巨页 */
#endif
    seL4_ModeObjectTypeCount    /*Z 架构相关的seL4内核对象类型数量 */
} seL4_seL4ArchObjectType;

/* allow seL4_X86_PDPTObject and seL4_IA32_PDPTObject to be used interchangeable */
#define seL4_IA32_PDPTObject seL4_X86_PDPTObject

#ifndef CONFIG_HUGE_PAGE
#define seL4_X64_HugePageObject 0xfffffffe
#endif

